Search for: All records

Dysregulations of epithelial-immune interactions frequently culminate in chronic inflammatory diseases of the skin, lungs, kidneys, and gastrointestinal tract. Yet, the intraepithelial processes that initiate and perpetuate inflammation in these organs are poorly understood. Here, by utilizing redox lipidomics we identified ferroptosis-associated peroxidation of polyunsaturated phosphatidylethanolamines in the epithelia of patients with asthma, cystic fibrosis, psoriasis, and renal failure. Focusing on psoriasis as a disease model, we used high-resolution mass spectrometry imaging and identified keratin 14–expressing (K14-expressing) keratinocytes executing a ferroptotic death program in human psoriatic skin. Psoriatic phenotype with characteristic Th1/Th17 skin and extracutaneous immune responses was initiated and maintained in a murine model designed to actuate ferroptosis in a fraction of K14+ glutathione peroxidase 4–deficient (Gpx4-deficient) epidermal keratinocytes. Importantly, an antiferroptotic agent, liproxstatin-1, was as effective as clinically relevant biological IL-12/IL-23/ TNF-α–targeting therapies or the depletion of T cells in completely abrogating molecular, biochemical, and morphological features of psoriasis. As ferroptosis in select epidermal keratinocytes triggers and sustains a pathological psoriatic multiorgan inflammatory circuit, we suggest that strategies targeting ferroptosis or its causes may be effective in preventing or ameliorating a variety of chronic inflammatory diseases. 

P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode, leaving many aspects of the language semantics up to individual compilation targets. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code, with support for only a few targets. Clearly neither of these artifacts is suitable for formal reasoning about P4 in general. This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a core calculus that models a fragment of P4. Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus overapproximates target-specific behaviors using non-determinism. We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We validated the core calculus with a proof of type-preserving termination. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.